(*This file describes security objectives of GP TEE defined in GlobePlatFrom Protection Profile.
Written by Zhejiang University, Hangzhou, China.*)

theory GPTEE_Objectives
  imports Main
begin

section "O_TA_AUTHENTICITY"
(*
FROM PP
==================
O.TA_AUTHENTICITY
The TEE shall verify the authenticity of the Trusted Applications’ binary code.

Application Note:
Verification of authenticity of TA code can be performed together with verification of the TEE firmware if 
both are bundled together or during the loading of the TA code in volatile memory.
===============
*)

locale O_TA_AUTHENTICITY
   =
  fixes verify :: "'bc ⇒ 'k ⇒ bool" 
    (* use a key 'k to authenticate whether a TA code 'bc is the CODE the TEE thinks *)
begin
  
end


section "O_CA_TA_IDENTIFICATION"

(* 
FROM PP
===============================
O.CA_TA_IDENTIFICATION

The TEE shall provide means to protect the identity of each Trusted Application from use by another 
resident Trusted Application and to distinguish Client Applications from Trusted Applications.

Application Note:
Client properties are managed either by the Regular OS or by the Trusted OS and these must ensure that 
a Client cannot tamper with its own properties in the following sense:
❖ The Client identity of a TA must always be determined by the Trusted OS and the determination 
of whether it is a TA or not must be as trustworthy as the Trusted OS itself; 
❖ When the Client identity corresponds to a TA, then the Trusted OS must ensure that the other 
Client properties are equal to the properties of the calling TA up to the same level of trustworthiness 
that the target TA places in the Trusted OS; 
❖ When the Client identity does not correspond to a TA, then the Regular OS is responsible for 
ensuring that the Client Application cannot tamper with its own properties. However, this 
information is not trusted by the Trusted OS.

note: after discussion, property here means identity
 *)

(*
(*version 2*)
locale O_CA_TA_IDENTIFICATION
   =
  (* The Client identity of a TA must always be determined by the Trusted OS *)
  fixes ta_client :: "'s ⇒ ('ta ⇀ 'cid)" (*search for TA client, if some, find one*)
  fixes ta_client_identification :: "'s⇒'cid⇒bool"(*judge the client_identity's type(TA/CA),if TA then True*)
  
  fixes ta_identification :: "'s⇒'cid⇒'ta"(*get ta's information by client_identity *)
  fixes ca_identification :: "'s⇒'cid⇒'ca"
  (* ta client identities are different *)
  assumes ta_ident: "∀s cid cid'. cid ≠ cid' ∧ ta_client_identification s cid ∧ ta_client_identification s cid'
                                        ⟶  ta_identification s cid ≠ ta_identification s cid'"

  fixes ta_props :: "'s ⇒ 'ta ⇒ 'tap" (* TA properties *)
  (*fixes ca_props :: "'s ⇒ 'ca ⇒ 'cap" (* CA properties *)*)
  fixes client_props :: "'s ⇒ 'cid ⇒ 'cp" (* client properties *)
  (* a func to decide whether the other Client properties are equal to the properties of TA *)
  fixes ta_ci_prop_eq :: "'cp ⇒ 'tap ⇒ bool" 
  (* Client properties are equal to the properties of the calling TA *)
  assumes tap_cip: "∀s ta. ta_client s ta ≠ None ⟶ 
            (ta_ci_prop_eq (client_props s (the (ta_client s ta))) (ta_props s ta))"
*)

locale O_CA_TA_IDENTIFICATION
   =
  (* The Client identity of a TA must always be determined by the Trusted OS *)
  fixes ta_client :: "'s ⇒ ('ta ⇀ 'cid)" (*search for TA client, if some, find one*)
  fixes ta_client_identification :: "'s⇒'cid⇒bool"(*judge the client_identity's type(TA/CA),if TA then True*)
  
  fixes ta_identification :: "'s⇒'ta⇒'cid"(*get ta's client_identity if it is as a client *)
  fixes ca_identification :: "'s⇒'ca⇒'cid"(*here CA is REE cause we dont identify different CA*)
  (* ta client identities are different *)
  assumes ta_ident: "∀s ta ta'. ta ≠ ta' ⟶  ta_identification s ta ≠ ta_identification s ta'"
  assumes ca_ta_ident: "∀s ta ca.  ta_identification s ta ≠ ca_identification s ca"

(*
  fixes ta_props :: "'s ⇒ 'ta ⇒ 'tap" (* TA properties *)
  (*fixes ca_props :: "'s ⇒ 'ca ⇒ 'cap" (* CA properties *)*)
  fixes client_props :: "'s ⇒ 'cid ⇒ 'cp" (* client properties *)
  (* a func to decide whether the other Client properties are equal to the properties of TA *)
  fixes ta_ci_prop_eq :: "'cp ⇒ 'tap ⇒ bool" 

  (* a func to decide whether the other Client properties are equal to the properties of TA *)
  fixes ta_ci_prop_eq :: "'cid ⇒ 'cid ⇒ bool"
  (* Client properties are equal to the properties of the calling TA *)
  assumes tap_cip: "∀s ta ta'. ta_client s ta ≠ None ⟶ 
            (ta_ci_prop_eq (client_props s (the (ta_client s ta))) (ta_props s ta))"
*)

  (* a func to decide whether the other Client properties are equal to the properties of TA *)
  fixes ta_ci_prop_eq :: "'cid ⇒ 'cid ⇒ bool"
  (* Client properties are equal to the properties of the calling TA *)
  assumes tap_cip: "∀s ta. ta_client s ta ≠ None ∧ ta_client_identification s (the (ta_client s ta))  ⟶ 
          (∃ta'. (ta_ci_prop_eq (the (ta_client s ta)) (ta_identification s ta')))"



begin

end



section "O_INSTANCE_TIME"

(*
FROM PP
======================
O.INSTANCE_TIME

The TEE shall provide TA instance time and shall ensure that this time is monotonic during TA instance 
lifetime – from the TA instance creation until the TA instance is destroyed – and not impacted by
transitions through low power states.
======================

*)

locale O_INSTANCE_TIME
   =
  fixes query_time::"'sc⇒'s⇒'tid⇒'instime::linorder"(*get TA instance time, system time + offset*)
  fixes trans::"'a ⇒ ('s × 's) set"
  (*The TEE shall ensure that this time is monotonic during TA instance lifetime*)
  assumes monotonic: "∀s sc a t tid. (s,t) ∈ trans a ⟶ (query_time sc s tid) ≤ (query_time sc t tid)"

(*it may not model here but in one part of our project, the time is updated by the timer*)


section "O_KEYS_USAGE"

(*
FROM PP
======================
O.KEYS_USAGE

The TEE shall enforce the cryptographic keys usage restrictions set by their creators.
//we only care about TA checksum, but not included here,this object may ignore
======================
*)

locale O_KEYS_USAGE
  =
  (*check whether the key is used by its owner*)
  fixes checksum::"'k⇒'kuser⇒bool"




section "O_OPERATION"

(*
O.OPERATION

The TEE shall ensure the correct operation of its security functions. In particular, the TEE shall:
o Protect itself against abnormal situations caused by programmer errors or violation of good 
practices by the REE (and the CAs indirectly) or by the TAs;
//maybe when TA get dead lock or call API without a proper order,

o Control access to its services by the REE and TAs: The TEE shall check the validity of any 
operation requested from either the REE or a TA, at any entry point into the TEE;

o Enter a secure state upon failure detection, without exposure of any sensitive data.

Application Note:
o Programmer errors or violation of good practices (e.g. that exploit multi-threading or 
context/session management) might become attack-enablers. However, the TEE must guarantee 
the stability and security of its resources and services independent of the REE, which may have 
been corrupted. In any case, a Trusted Application must not be able to use a programmer error 
on purpose to circumvent the TEE security functionality.

o Software in the REE must not be able to call directly to TEE resources or functions. The REE 
software must go through protocols such that the Trusted OS or Trusted Application performs the 
verification of the acceptability of the operation that the REE software has requested.
*)

locale O_OPERATION
   =
  (*Control access to its services by the REE and TAs*)
  fixes valid_ca_access::"'s⇒'a⇒'ca⇒bool"(*1. whether CA can call some API. 
                  2. whether obey the policy for controlling access to TA and TEE execution spaces*)
  fixes valid_ta_access::"'s⇒'a⇒'ta⇒bool"

  (*the allowed API for TA and CA are different
  assumes access_diff:"∀s a ca ta. valid_ca_access s a ca ≠ valid_ta_access s a ta"*)

  (*Programmer errors or violation of good practices*)
  fixes valid_ca_action::"'s⇒'a⇒'ca⇒bool"
  fixes valid_ta_action::"'s⇒'a⇒'ta⇒bool"
  (*
  with three dimension: 1. the action is a defined API?(unexpected commands) 
                        2. bad parameter?(programmer error)
                        3. other programmer error
  *)
  fixes move_to_secure_state::"'s⇒'s"(*Enter a secure state,like trans1, but different actions*)
  fixes secure_state::"'s⇒bool"(*judge whether the state is secure*)
  fixes trans::"'a ⇒ ('s × 's) set"
  fixes failure_detect::"'s⇒bool"
  (*Protect itself against abnormal situations caused by programmer errors or violation of good practices*)
  assumes action_cor_use:"∀s a ca ta. ¬(valid_ca_action s a ca) ∨ ¬(valid_ta_action s a ta) 
                          ⟶ failure_detect s"
  (*Control access to its services by the REE and TAs*)
  assumes access_cor_use:"∀s a ca ta. ¬(valid_ca_access s a ca) ∨ ¬(valid_ta_access s a ta) 
                          ⟶ failure_detect s"
  (*the TEE shall Enter a secure state upon failure detection*)
  assumes "∀s s'. s' = move_to_secure_state s ∧ failure_detect s ⟶ secure_state s'"






section "O_ISOLATION"
  
(*
Isolation includes the 4 objectives below:

- O.RUNTIME_CONFIDENTIALITY

The TEE shall ensure that confidential TEE runtime data and TA data and keys are protected against 
unauthorized disclosure. In particular:
o The TEE shall not export any sensitive data, random numbers or secret keys to the REE;
o The TEE shall grant access to sensitive data, random numbers or secret keys only to authorized 
TAs;
o The TEE shall clean up sensitive resources as soon as it can determine that their values are no 
longer needed.

- O.RUNTIME_INTEGRITY

The TEE shall ensure that the TEE firmware, TEE runtime data, TA code, and TA data and keys are 
protected against unauthorized modification at runtime when stored in volatile memory

- O.TA_ISOLATION

The TEE shall isolate the TAs from each other: Each TA shall access its own execution and storage space, 
which is shared among all the instances of the TA but separated from the spaces of any other TA.
Application Note:
This objective contributes to the enforcement of the confidentiality and integrity of TA data.

- O.TEE_ISOLATION

The TEE shall prevent the REE and the TAs from accessing the TEE’s own execution and storage space 
and resources.
Application Note:
This objective contributes to the enforcement of the correct execution of the TEE. Note that resource 
allocation can change during runtime as long as it does not break isolation between resources used by the 
TEE and the REE/TAs.
// maybe tee's accessing ta's data is allowed
*)


locale O_ISOLATION
   =
  fixes s0 :: 's
  fixes trans :: "'a ⇒ ('s × 's) set" (* state machine of the whole system *)
  fixes domain :: "'s ⇒ 'a ⇒ 'd option" (* domain of actions *)
 (* fixes elist :: "'s⇒('c×'b) list"*)
 fixes elist ::"'s⇒'const"
  fixes vpeq :: "'s ⇒ 'd ⇒ 's ⇒ bool"  ("(_ ∼ _ ∼ _)") 
  fixes interference :: "'d ⇒ 'd ⇒ bool" ("(_ ↝ _)")
(*
  fixes write_interference :: "'d ⇒ 'd ⇒ bool" ("(_ ↝ _)")(*including sensitive data and params*)
  fixes ta_data::"'s⇒'d⇒'data"(*ta runtime data, parameter not included*)
  fixes tee_data::"'s⇒'d⇒'data"(*tee runtime data, parameter not included*)
  (*because REE data can be accessed by all, so we don't model it*)
  fixes access::"'s⇒'d⇒'data⇒bool"(*ta/tee runtime data access management*)
  fixes clean_up::"'s⇒'data⇒bool"(*The TEE shall clean up sensitive resources*)
  fixes read_interference :: "'d ⇒ 'd ⇒ bool" ("(_↪_)")
*)

(*
   // in this project TA is TA instance so we may not distinguish them
*)

  fixes TEE :: 'd (* the TEE domain *)
  fixes REE :: 'd (* the REE domain *)
  fixes TA_domain :: "'s⇒ 'ta ⇒ 'd"  (* domain id of TAs *)
(* fixes CA_domain :: "'ca ⇒ 'd"*)  (* domain id of CAs *) 
    (* CAs as clients have to be identified, as well as their actions, 
    so we consider each CA as an identity. When define security, we consider them as the whole REE domain  *)
  (*
  assumes "TEE ≠ REE"
    and   "∀ta s. TA_domain s ta ≠ TEE ∧ TA_domain s ta ≠ REE"
    and   "∀s. inj (TA_domain s)"
    and   "∀d s. d = TEE ∨ d = REE ∨ (∃ta. TA_domain s ta = d)" 
  *)
  (*we can write this in specification because we proof security in requirement layer,not secure layer*) 



   (* CAs as clients have to be identified, as well as their actions, 
      so we consider each CA as a domain. When define security, we consider them as the whole REE domain  *)

(* 
  (*The TEE shall not export any sensitive data, random numbers or secret keys to the REE*)
  assumes ree_no_access: "∀s data d. (data = ta_data s d) ∨ (data = tee_data s d) ⟶ ¬ access s REE data"
  assumes 
    ta_data_diff:"∀s ta ta'. ta_data s (TA_domain ta) ≠ ta_data s (TA_domain ta')"
    and ta_tee_diff:"∀s ta. ta_data s (TA_domain ta) ≠ tee_data s TEE"
    (*The TEE shall grant access to sensitive data, random numbers or secret keys only to authorized TAs*)
    (*Each TA shall access its own execution and storage space*)
    and ta_data_iso:"∀s ta data. access s (TA_domain ta) data ⟶ data = (ta_data s (TA_domain ta)) "
    (*The TEE shall prevent the REE and the TAs from accessing the TEE’s own execution and storage space and resources.*)
    and ta_tee_iso:"∀s ta. TA_domain ta ≠ TEE ⟶ ¬ access s (TA_domain ta) (tee_data s TEE)"
*)

  assumes 
    vpeq_transitive_lemma : "∀ s t r d. (s ∼ d ∼ t) ∧ (t ∼ d ∼ r) ⟶ (s ∼ d ∼ r)" and
    vpeq_symmetric_lemma : "∀ s t d. (s ∼ d ∼ t) ⟶ (t ∼ d ∼ s)" and
    vpeq_reflexive_lemma : "∀ s d. (s ∼ d ∼ s)" and
   (* tee_vpeq : "∀s t a. (s ∼ TEE ∼ t) ⟶ (domain s a) = (domain t a)" and*)
    tee_intf_all : "∀d. (TEE ↝ d)" and
    no_intf_tee : "∀d. (d ↝ TEE) ⟶ d = TEE" and
    interf_reflexive: "∀d. (d ↝ d)" 
(*
    tee_vpeq : "∀s t. (s ∼ TEE ∼ t) ⟶ (tee_data s TEE) = (tee_data t TEE)" and
    ta_vpeq : "∀s t ta. (s ∼ TA_domain ta ∼ t) ⟶ ta_data s (TA_domain ta) = ta_data t (TA_domain ta)" and
*) 


begin

definition non_interference :: "'d ⇒ 'd ⇒ bool" ("(_ ∖↝ _)")
  where "(u ∖↝  v) ≡ ¬ (u ↝ v)"

(*definition non_read_interference :: "'d ⇒ 'd ⇒ bool" ("(_ ∖↪ _)")
  where "(u ∖↪  v) ≡ ¬ (u ↪ v)"
*)


(*state transition after the execution of an event list in which each event is executed by function "trans"*)
primrec run::"'a list⇒('s × 's) set" where
  run_Nil: "run [] = Id" |
  run_Cons: "run (a#as) = trans a O run as"

(*judge whether s' is reachable after the execution of an event list with an initial state s*)
definition reachable::"'s⇒'s⇒bool" where
  "reachable s1 s2 ≡ (∃as. (s1,s2) ∈ run as)"
  
(*judge whether s is reachable from initial state s0*)
definition reachable0 :: "'s ⇒ bool"  where
  "reachable0 s ≡ reachable s0 s"

definition execute :: "'a list ⇒ 's ⇒ 's set" 
      where "execute as s = Image (run as) {s} " 


declare non_interference_def[cong] and reachable_def[cong] and reachable0_def[cong] and execute_def[cong] and run.simps(1)[cong] and
            run.simps(2)[cong]

    lemma reachable_s0 : "reachable0 s0"
      using reachable0_def reachable_def run_Nil by blast
      
    
    lemma reachable_self : "reachable s s"
      using reachable_def run.simps(1) by fastforce

    lemma reachable_trans : "(s,s')∈trans a ⟹ reachable s s'"
      proof-
        assume a0: "(s,s')∈trans a"
        then have "(s,s')∈run [a]" by auto          
        then show ?thesis using reachable_def by blast 
      qed

    lemma run_trans : "∀C T V as bs. (C,T)∈run as ∧ (T,V)∈run bs ⟶ (C,V)∈run (as@bs)"
      proof -
      {
        fix T V as bs
        have "∀C. (C,T)∈run as ∧ (T,V)∈run bs ⟶ (C,V)∈run (as@bs)"
          proof(induct as)
            case Nil show ?case by simp
          next
            case (Cons c cs)
            assume a0: "∀C. (C, T) ∈ run cs ∧ (T, V) ∈ run bs ⟶ (C, V) ∈ run (cs @ bs)"
            show ?case
              proof-
              {
                fix C
                have "(C, T) ∈ run (c # cs) ∧ (T, V) ∈ run bs ⟶ (C, V) ∈ run ((c # cs) @ bs) "
                  proof
                    assume b0: "(C, T) ∈ run (c # cs) ∧ (T, V) ∈ run bs"
                    from b0 obtain C' where b2: "(C,C')∈trans c ∧ (C',T)∈run cs" by auto
                    with a0 b0 have "(C',V)∈run (cs@bs)" by blast
                    with b2 show "(C, V) ∈ run ((c # cs) @ bs)"
                      using append_Cons relcomp.relcompI run_Cons by auto 
                  qed
              }
              then show ?thesis by auto
              qed
          qed
      }
      then show ?thesis by auto
      qed

    lemma reachable_transitive : "⟦reachable C T; reachable T V⟧ ⟹ reachable C V"
      proof-
        assume a0: "reachable C T"
        assume a1: "reachable T V"
        from a0 have "C = T ∨ (∃as. (C,T)∈run as)" by simp
        then show ?thesis
          proof
            assume b0: "C = T"
            show ?thesis 
              proof -
                from a1 have "T = V ∨ (∃as. (T,V)∈run as)" by simp
                then show ?thesis
                  proof
                    assume c0: "T=V"
                    with a0 show ?thesis by auto
                  next
                    assume c0: "(∃as. (T,V)∈run as)"
                    then show ?thesis using a1 b0 by auto 
                  qed
              qed
          next
            assume b0: "∃as. (C,T)∈run as"
            show ?thesis
              proof -
                from a1 have "T = V ∨ (∃as. (T,V)∈run as)" by simp
                then show ?thesis
                  proof
                    assume c0: "T=V"
                    then show ?thesis using a0 by auto 
                  next
                    assume c0: "(∃as. (T,V)∈run as)"
                    from b0 obtain as where d0: "(C,T)∈run as" by auto
                    from c0 obtain bs where d1: "(T,V)∈run bs" by auto
                    then show ?thesis using d0  run_trans by fastforce
                  qed
              qed
          qed
      qed

    lemma reachableStep : "⟦reachable0 C; (C,C')∈trans a⟧ ⟹ reachable0 C'"
    by (meson reachable0_def reachable_def reachable_trans run_trans)
     
     
    lemma reachable0_reach : "⟦reachable0 C; reachable C C'⟧ ⟹ reachable0 C'"
    by (simp add: reachable_transitive)
      
    declare reachable_def[cong del] and reachable0_def[cong del]

subsection "security properties"

definition integrity :: "bool" where
      "integrity ≡ ∀ a d s s'. reachable0 s ∧ ((the (domain s a)) ∖↝ d) ∧ (s, s') ∈ trans a  ⟶ (s ∼ d ∼ s')"
      
definition integrity_e :: "'a⇒bool" where
      "integrity_e a ≡ ∀ d s s'. reachable0 s ∧ ((the (domain s a)) ∖↝ d) ∧ (s, s') ∈ trans a  ⟶ (s ∼ d ∼ s')"
   


definition confidentiality :: "bool" where
      "confidentiality ≡ ∀a d s t. reachable0 s ∧ reachable0 t ∧ (s ∼ d ∼ t) ∧ (domain s a = domain t a)
                                ∧(elist s=elist t)∧(((the (domain s a)) ↝ d) ⟶ (s ∼ (the (domain s a)) ∼ t)) ⟶ 
                                (∀ s' t'. (s, s') ∈ trans a  ∧ (t, t') ∈ trans a ⟶ (s' ∼ d ∼ t'))"

definition confidentiality_e :: "'a⇒bool" where
      "confidentiality_e a ≡ ∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼ d ∼ t) ∧ (domain s a = domain t a)
                                ∧(elist s=elist t)∧(((the (domain s a)) ↝ d) ⟶ (s ∼ (the (domain s a)) ∼ t)) ⟶ 
                                (∀ s' t'. (s, s') ∈ trans a  ∧ (t, t') ∈ trans a ⟶ (s' ∼ d ∼ t'))"

definition weak_confidentiality :: "bool" where
      "weak_confidentiality ≡ ∀a d s t. reachable0 s ∧ reachable0 t ∧ (s ∼ d ∼ t) ∧ (domain s a = domain t a)
                                ∧(elist s=elist t)∧(((the (domain s a)) ↝ d) ∧ (s ∼ (the (domain s a)) ∼ t)) ⟶ 
                                (∀ s' t'. (s, s') ∈ trans a  ∧ (t, t') ∈ trans a ⟶ (s' ∼ d ∼ t'))"

definition weak_confidentiality_e :: "'a⇒bool" where
      "weak_confidentiality_e a ≡ ∀d s t. reachable0 s ∧ reachable0 t ∧ (s ∼ d ∼ t) ∧ (domain s a = domain t a)
                                ∧(elist s=elist t)∧(((the (domain s a)) ↝ d) ∧ (s ∼ (the (domain s a)) ∼ t)) ⟶ 
                                (∀ s' t'. (s, s') ∈ trans a  ∧ (t, t') ∈ trans a ⟶ (s' ∼ d ∼ t'))"


declare confidentiality_def[cong] and confidentiality_e_def[cong] and
          weak_confidentiality_def[cong] and weak_confidentiality_e_def[cong] and
          integrity_def[cong] and integrity_e_def[cong]

lemma confidentiality_all_evt: "confidentiality = (∀a. confidentiality_e a)"
    by simp

lemma weak_confidentiality_all_evt: "weak_confidentiality = (∀a. weak_confidentiality_e a)"
    by simp

lemma integrity_all_evt: "integrity = (∀a. integrity_e a)"
    by simp

lemma weak_with_step_cons:
      assumes p1:weak_confidentiality
        and   p2:integrity
      shows   confidentiality
      proof -
      {
        fix d a s t s' t'
        have "reachable0 s ∧ reachable0 t ⟶ (s ∼ d ∼ t) ∧ (domain s a = domain t a) ∧(elist s=elist t)∧ 
              (((the (domain s a)) ↝ d) ⟶ (s ∼ (the (domain s a)) ∼ t)) ⟶ (s,s')∈trans a ∧ (t,t')∈trans a
              ⟶ (s' ∼ d ∼ t')" 
           proof -
           {
             assume aa:"reachable0 s ∧ reachable0 t"
             assume a0:"s ∼ d ∼ t"
             assume a1:"(domain s a = domain t a)"
             assume a11:"(elist s=elist t)"
             assume a2:"((the (domain s a)) ↝ d) ⟶ (s ∼ (the (domain s a)) ∼ t)"
             assume a3: "(s,s')∈trans a ∧ (t,t')∈trans a"
             have "s' ∼ d ∼ t'"
              proof(cases "(the (domain s a)) ↝ d")
                assume b0:"(the (domain s a)) ↝ d"
                show ?thesis using aa a0 a1 a2 b0 p1 weak_confidentiality_def a3 a11 by blast 
                next
                assume b1:"¬((the (domain s a)) ↝ d)"
                have b2:"(domain s a) = (domain t a)" by (simp add: a1 )
                with b1 have b3:"¬((the (domain t a)) ↝ d)" by auto
                then have b4:"s∼d∼s'" using aa b1  p2 a3  by fastforce 
                then have b5:"t∼d∼t'" using aa b3 p2 a3 by fastforce
                then show ?thesis using a0 b4 vpeq_symmetric_lemma vpeq_transitive_lemma by blast
              qed
           }
           then show ?thesis by auto
           qed
      }
      then show ?thesis using confidentiality_def  by blast
      qed








(*
subsection "New Integrity Definition"
(*TA cant modify REE*)
definition REE_TA_integrity :: "bool" where
      "REE_TA_integrity ≡ ∀ a s s'. reachable0 s ∧ ((the (domain s a)) ≠ REE) ∧ ((the (domain s a)) ≠ TEE)
                                     ∧ s' = trans s a  ⟶ (s ∼ REE ∼ s')"
(*REE cant modify TA*)
definition TA_REE_integrity :: "bool" where
      "TA_REE_integrity ≡ ∀ a d s s'. reachable0 s ∧ ((the (domain s a)) = REE) ∧ s' = trans s a  
                                ⟶ (s ∼ d ∼ s') ∧ (d ≠ TEE) ∧ (d ≠ REE) "
(*TA cant modify TEE*)
definition TEE_TA_integrity :: "bool" where
      "TEE_TA_integrity ≡ ∀ a s s'. reachable0 s ∧ ((the (domain s a)) ≠ REE) ∧ ((the (domain s a)) ≠ TEE)
                                     ∧ s' = trans s a  ⟶ (s ∼ TEE ∼ s')"
(*REE cant modify TEE*)
definition TEE_REE_integrity :: "bool" where
      "TEE_REE_integrity ≡ ∀ a s s'. reachable0 s ∧ ((the (domain s a)) = REE)
                                     ∧ s' = trans s a  ⟶ (s ∼ TEE ∼ s')"
(*TA cant modify TA*)
definition TA_TA_integrity :: "bool" where
      "TA_TA_integrity ≡ ∀ a d s s'. reachable0 s ∧ ((the (domain s a)) ≠ REE) ∧ ((the (domain s a)) ≠ TEE) 
                                      ∧ ((the (domain s a)) ≠ d)∧ s' = trans s a  
                                      ⟶ (s ∼ d ∼ s') ∧ (d ≠ TEE) ∧ (d ≠ REE)"

(*So we define ↝ as write access, a↝b means a can modify memory in domain b*)
definition new_integrity :: "bool" where
      "new_integrity ≡ ∀ a d s s'. reachable0 s ∧ ((the (domain s a)) ∖↝ d) ∧ s' = trans s a  ⟶ (s ∼ d ∼ s')"

subsection "New Confidentiality Definition"

(*REE cant read TA*)
definition REE_TA_confidentiality :: "bool" where
      "REE_TA_confidentiality ≡ ∀a s t. reachable0 s ∧ reachable0 t ∧ (s ∼ REE ∼ t) ∧ (domain s a = domain t a)
                                ∧((the (domain s a)) ≠ REE) ∧ ((the (domain s a)) ≠ TEE)  ⟶ 
                                (∀ s' t'. s' = trans s a  ∧ t' = trans t a ⟶ (s' ∼ REE ∼ t'))"
(*delete ∧ (s ∼ (the (domain s a)) ∼ t) for all confidentiality*)

(*REE cant read TEE*)
definition REE_TEE_confidentiality :: "bool" where
      "REE_TEE_confidentiality ≡ ∀a s t. reachable0 s ∧ reachable0 t ∧ (s ∼ REE ∼ t) ∧ (domain s a = domain t a)
                                ∧ ((the (domain s a)) = TEE) ⟶ 
                                (∀ s' t'. s' = trans s a  ∧ t' = trans t a ⟶ (s' ∼ REE ∼ t'))"

(*TA cant read TA*)
definition TA_TA_confidentiality :: "bool" where
      "TA_TA_confidentiality ≡ ∀a d s t. reachable0 s ∧ reachable0 t ∧ (s ∼ d ∼ t) ∧ (domain s a = domain t a)
                                ∧((the (domain s a)) ≠ REE) ∧ ((the (domain s a)) ≠ TEE) ∧ ((the (domain s a)) ≠ d) 
                                     ⟶ 
                                (∀ s' t'. s' = trans s a  ∧ t' = trans t a ⟶ (s' ∼ d ∼ t')) ∧ (d ≠ TEE) ∧ (d ≠ REE)"

(*TA cant read TEE*)
(*TBD: TA need to access TA bin in TEE's memory when initializing*)
definition TA_TEE_confidentiality :: "bool" where
      "TA_TEE_confidentiality ≡ ∀a d s t. reachable0 s ∧ reachable0 t ∧ (s ∼ d ∼ t) ∧ (domain s a = domain t a)
                                ∧((the (domain s a)) =TEE)  ⟶ 
                                (∀ s' t'. s' = trans s a  ∧ t' = trans t a ⟶ (s' ∼ d ∼ t')) ∧ (d ≠ TEE) ∧ (d ≠ REE)"

(*define ↪ as read access, a↪b means b can read data in domain a*)

definition new_confidentiality :: "bool" where
        "new_confidentiality ≡ ∀a d s t. reachable0 s ∧ reachable0 t ∧ (s ∼ d ∼ t) ∧ (domain s a = domain t a)
                                ∧((the (domain s a)) ∖↪ d) ⟶ 
                                (∀ s' t'. s' = trans s a  ∧ t' = trans t a ⟶ (s' ∼ d ∼ t'))"
*)

end

end